
; Copyright (c) 2015 Microsoft Corporation
(declare-const transition_0_n Int)
(declare-const transition_1_n Int)
(declare-const transition_2_n Int)
(declare-const transition_3_n Int)
(declare-const transition_4_n Int)
(declare-const transition_5_n Int)
(declare-const transition_6_n Int)
(declare-const transition_7_n Int)
(declare-const transition_8_n Int)
(declare-const transition_9_n Int)
(declare-const transition_10_n Int)
(declare-const transition_11_n Int)
(declare-const transition_12_n Int)
(declare-const transition_13_n Int)
(declare-const transition_14_n Int)
(declare-const transition_15_n Int)
(declare-const transition_16_n Int)
(declare-const transition_17_n Int)
(declare-const transition_18_n Int)
(declare-const transition_19_n Int)
(declare-const transition_20_n Int)
(declare-const transition_21_n Int)
(declare-const transition_22_n Int)
(declare-const transition_23_n Int)
(declare-const transition_24_n Int)
(declare-const transition_25_n Int)
(declare-const transition_26_n Int)
(declare-const transition_27_n Int)
(declare-const transition_28_n Int)
(declare-const transition_29_n Int)
(declare-const transition_30_n Int)
(declare-const transition_31_n Int)
(declare-const transition_32_n Bool)
(declare-const transition_33_n Int)
(declare-const transition_34_n Int)
(declare-const transition_35_n Int)
(declare-const transition_36_n Int)
(declare-const transition_37_n Int)
(declare-const transition_38_n Int)
(declare-const transition_39_n Int)
(declare-const transition_40_n Int)
(declare-const transition_41_n Int)
(declare-const transition_42_n Int)
(declare-const transition_43_n Int)
(declare-const transition_44_n Int)
(declare-const transition_45_n Int)
(declare-const transition_46_n Int)
(declare-const transition_47_n Int)
(declare-const transition_48_n Int)
(declare-const transition_49_n Int)


(push)
(assert (and
(or (<= transition_6_n 4)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (<= transition_12_n 3)
    (<= transition_7_n 3)
    (>= transition_5_n 5)
    (<= transition_8_n (- 1))
    (>= transition_8_n 1)
    (>= transition_6_n 6)
    transition_32_n)
(or (>= transition_12_n 3)
    (not transition_32_n)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_5_n 5)
    (>= transition_7_n 3))
(or (>= transition_12_n 3)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_5_n 5)
    (>= transition_7_n 3))
(or (>= transition_12_n 3)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3))
(or (>= transition_12_n 4)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3))
(or (<= transition_5_n 0)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (<= transition_12_n 2)
    (>= transition_12_n 4)
    (>= transition_7_n 3))
(or (>= transition_8_n 1)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3)
    (>= transition_12_n 4)
    (<= transition_8_n (- 1)))
(or (>= transition_5_n 1)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3)
    (<= transition_8_n (- 1))
    (>= transition_8_n 1))
(or (>= transition_8_n 1)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_5_n 5)
    (>= transition_7_n 3)
    (<= transition_8_n (- 1)))
(or (>= transition_7_n 3)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (<= transition_5_n 0)
    (>= transition_5_n 5))
(or (<= transition_12_n 3)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3)
    (>= transition_5_n 1))
(or (>= transition_12_n 4)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3))
(or (>= transition_7_n 3)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0))
(or (<= transition_12_n 3)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0))
(or (<= transition_12_n 2)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0))
(or (<= transition_0_n 0) (not (>= transition_5_n 5)) (>= transition_0_n 2))
(or (<= transition_5_n 0)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_12_n 3))
(or (>= transition_12_n 3) (>= transition_0_n 2) (<= transition_0_n 0))
(or (>= transition_12_n 4) (>= transition_0_n 2) (<= transition_0_n 0))
(or (<= transition_0_n 0) (>= transition_0_n 2))
(or (<= transition_8_n 0) (>= transition_0_n 2))
))

(apply unit-subsume-simplify)
(check-sat)
(pop)

(push)
(assert (and
(<= transition_41_n (- 1))
(<= transition_40_n (- 1))
(<= transition_39_n (- 1))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    transition_32_n
    (not (>= transition_6_n 5))
    (not (<= transition_6_n 5))
    (<= transition_0_n 2)
    (not (<= transition_8_n 0))
    (not (>= transition_8_n 0))
    (<= transition_12_n 3)
    (<= transition_7_n 3))
(or (>= transition_0_n 4)
    (not transition_32_n)
    (>= transition_5_n 5)
    (<= transition_0_n 2)
    (>= transition_12_n 3)
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (<= transition_0_n 2)
    (>= transition_12_n 3)
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (not (>= transition_5_n 5))
    (<= transition_0_n 2)
    (>= transition_12_n 3)
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (not (>= transition_5_n 5))
    (not (<= transition_12_n 3))
    (not (>= transition_12_n 3))
    (<= transition_0_n 2)
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (not (<= transition_12_n 3))
    (not (>= transition_12_n 3))
    (<= transition_0_n 2)
    (<= transition_5_n 0)
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (not (<= transition_12_n 3))
    (not (>= transition_12_n 3))
    (<= transition_0_n 2)
    (not (<= transition_8_n 0))
    (not (>= transition_8_n 0))
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (<= transition_0_n 2)
    (not (<= transition_8_n 0))
    (not (>= transition_8_n 0))
    (<= transition_12_n 3)
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (<= transition_0_n 2)
    (<= transition_5_n 0)
    (<= transition_12_n 3)
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (<= transition_0_n 2)
    (<= transition_12_n 3)
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (not (<= transition_12_n 3))
    (not (>= transition_12_n 3))
    (<= transition_0_n 2)
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (not (>= transition_5_n 5))
    (<= transition_0_n 2)
    (<= transition_12_n 3)
    (>= transition_7_n 3))
(or (>= transition_0_n 4)
    (not (>= transition_5_n 5))
    (<= transition_0_n 2)
    (<= transition_12_n 3))
(or (>= transition_0_n 4)
    (not (>= transition_5_n 5))
    (not (<= transition_12_n 3))
    (not (>= transition_12_n 3))
    (<= transition_0_n 2))
(or (>= transition_0_n 4)
    (not (>= transition_5_n 5))
    (<= transition_0_n 2)
    (>= transition_12_n 3))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (<= transition_0_n 2)
    (<= transition_5_n 0)
    (>= transition_12_n 3))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (<= transition_0_n 2)
    (>= transition_12_n 3))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (not (<= transition_12_n 3))
    (not (>= transition_12_n 3))
    (<= transition_0_n 2))
(or (>= transition_0_n 4)
    (>= transition_5_n 5)
    (<= transition_0_n 2)
    (<= transition_12_n 3))
(<= transition_2_n 0)
(<= transition_42_n (- 1))
(>= transition_0_n 17)
(<= transition_36_n (- 1))
(<= transition_37_n (- 1))
(<= transition_38_n (- 1))))


(apply unit-subsume-simplify)
(check-sat)
(pop)

(push)
(assert (and
(or (<= transition_6_n 4)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (<= transition_12_n 3)
    (<= transition_7_n 3)
    (>= transition_5_n 5)
    (<= transition_8_n (- 1))
    (>= transition_8_n 1)
    (>= transition_6_n 6)
    transition_32_n)
(or (>= transition_5_n 1)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (<= transition_12_n 3))
(or (>= transition_12_n 3)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_5_n 5)
    (>= transition_7_n 3))
(or (>= transition_12_n 3)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3))
(or (>= transition_12_n 4)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3))
(or (<= transition_5_n 0)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (<= transition_12_n 2)
    (>= transition_12_n 4)
    (>= transition_7_n 3))
(or (>= transition_8_n 1)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3)
    (>= transition_12_n 4)
    (<= transition_8_n (- 1)))
(or (>= transition_5_n 1)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3)
    (<= transition_8_n (- 1))
    (>= transition_8_n 1))
(or (>= transition_8_n 1)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_5_n 5)
    (>= transition_7_n 3)
    (<= transition_8_n (- 1)))
(or (>= transition_7_n 3)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (<= transition_5_n 0)
    (>= transition_5_n 5))
(or (<= transition_12_n 3)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3)
    (>= transition_5_n 1))
(or (>= transition_12_n 4)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_7_n 3))
(or (>= transition_7_n 3)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0))
(or (<= transition_12_n 3)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0))
(or (<= transition_12_n 2)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0))
(or (<= transition_5_n 0)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_12_n 3))
(or (>= transition_12_n 3) (>= transition_0_n 2) (<= transition_0_n 0))
(or (>= transition_12_n 4) (>= transition_0_n 2) (<= transition_0_n 0))
(or (<= transition_0_n 0) (>= transition_0_n 2))
(or (<= transition_8_n 0) (>= transition_0_n 2))
(or (>= transition_5_n 5)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (<= transition_12_n 3))
(or (>= transition_5_n 5)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (<= transition_5_n 0)
    (<= transition_12_n 2))
(or (>= transition_5_n 1)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (<= transition_12_n 2))
(or (>= transition_5_n 1) (>= transition_0_n 2) (<= transition_0_n 0))
(or (>= transition_5_n 5) (>= transition_0_n 2) (<= transition_0_n 0))
(or (>= transition_12_n 3)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0))
(or (>= transition_12_n 4)
    (not (>= transition_5_n 5))
    (>= transition_0_n 2)
    (<= transition_0_n 0))
(or (<= transition_0_n 0) (not (>= transition_5_n 5)) (>= transition_0_n 2))
(or (>= transition_12_n 3)
    (not transition_32_n)
    (>= transition_0_n 2)
    (<= transition_0_n 0)
    (>= transition_5_n 5)
    (>= transition_7_n 3))
))
(apply unit-subsume-simplify)
(check-sat)
(pop)


